In recent years, formal methods have undergone a fast development. The authors give a brief review on the formal methods used in software and hardware verification. The main thread of the analysis consists of descriptions of logical systems and their related verification techniques and tools. The purpose is to help engineers to select formal tools and apply them to their work. This paper starts with a review of automated proving techniques based on propositional logic and temporal logic, including SAT, BDD, model checking, and SMT. For first order logic based theorem provers, the authors discuss ACL2, VDM method and B method. Among proof assistants which are based on higher order logics, the authors pick HOL, PVS and COQ. Advancements in commercial formal verification tools are discussed.

The authors analyse a PLC competition quiz machine program and proves a set of properties using the COQ theorem prover. These properties reveal that only half of output states would be reachable and describe the transition relation over these states in an abstract way. Based on theseresults the author sintroducethe notion of logic automata as a complete description of this PLC program. The authors also point out that the program may produce unfair response in rare situations.